$\forall$$x$, $y$:Atom1. ($\uparrow$$x$ =a1 $y$) $\Leftarrow\!\Rightarrow$ ($x$ = $y$)